ds:fpf(Id; x.Type{i}), da:fpf(Knd; k.Type{i}). ecl(ds; da)  Type{i'} 

latex

Definitions	x:A. B(x), t  T, ecl(ds; da), x. t(x), x(s)
Lemmas	Knd wf, decl-state wf, ma-valtype wf, bool wf, nat wf, fpf wf, Id wf